/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

import alloy.util.Dbg;
import alloy.util.Util;

/**
 * An annotation on a BooleanFormula that says this formula matches this Boolean template with
 * this argument list.  The annotation is attached to the Boolean formula by the package {@link alloy.sharbool},
 * which calls {@link BooleanFormula#recordCachingInfo}.  The invariant that must be obeyed by
 * the Boolean template annotations is described next.
 * <p>
 * Take {@link BooleanFormula}s f1,f2 {@linkplain BooleanFormula#recordCachingInfo annotated} with {@link BoolTemplateInstance}s
 * t1,t2 respectively.  If t1.templCacheId==t2.templCacheId, then if A1,A2 are two assignments to {@linkplain BoolSwitch switches} where A1 sets all the
 * free switches in f1, and A2 sets all the free switches in f2, 
 * and 
 * <p>
 * @see alloy.sharbool
 * @see alloy.sharbool.TemplateDetectVisitor#_markSharedBooleanFormulas
 */
class BoolTemplateInstance {
    /**
     * The ID of the Boolean template.  Two {@link BooleanFormula}s are {@linkplain BooleanFormula#recordCachingInfo annotated}
     * with {@link BoolTemplateInstance}s that have the same {@link #templCacheId} if grounding out these
     * formulas might yield identical Boolean formulas.
     */
    final int templCacheId;

    /**
     * The key that is used to determine when two lifted Boolean formulas will ground out to identical ground
     * formulas during grounding-out.  Each element of templCacheKey is a {@linkplain BooleanFormula#isConstantValued constant-valued}
     * BooleanFormula, i.e. one that does not mention any literals.  Any leaves of such a formula are either constants,
     * or {@linkplain VarConst switchable constants} -- so for any given assignment to the {@linkplain BoolSwitch switches} on which
     * this BooleanFormula's switchable constants depend, the formula simplifies to a single Boolean value (true or false).
     *
     * @see #computeTemplKey
     */
    final BooleanFormula[] templCacheKey;

    //
    // The following two fields are used for creating a compressed integer representation of the value of templCacheKey.
    //

    /**
     * The partitioning of {@link #templCacheKey} into a sequence of arguments.  Used for compressing the integer
     * representation of the value of {@link #templCacheKey}.  E.g. templCacheKey may consist of three arguments
     * of width 2,3,4 respectively; then the length of templCacheKey would be 2+3+4=9, and the value of
     * templArgScopes[] would be {2,3,4}.
     
     * @see #computeTemplKey
     */
    final int[] templArgScopes;

    /**
     * For each element of templArgScopes, information about the kinds of values that argument
     * can take during grounding out.  The possible values are:
     * <ul>
     * <li>{@link BooleanFormula#MULT_SET} -- all binary combinations are possible
     * <li>{@link BooleanFormula#MULT_SCALAR} -- exactly one bit out of the bits of the argument is
     * true at any time.  this lets {@link #computeTemplKey} represent this argument using a compressed
     * (logarithmic) representation.</li>
     * <li>{@link BooleanFormula#MULT_OPTION} -- at most one bit out of the bits of this argument
     * is true at any time.  this lets {@link #computeTemplKey} represent this argument using a compressed
     * (logarithmic) representation.
     * </ul>
     *
     * @see #computeTemplKey
     */
    final int[] templArgMults;

    //////////////
    // Methods //
    ////////////
    
    BoolTemplateInstance(final int templCacheId_,
            final BooleanFormula[] templCacheKey_,
            final int[] templArgScopes_,
            final int[] templArgMults_) { 
        this.templCacheId = templCacheId_;
        this.templCacheKey = templCacheKey_;
        this.templArgScopes = templArgScopes_;
        this.templArgMults = templArgMults_;
    }

    /**
     * Return the {@linkplain #templCacheId ID} of the Boolean template.
     * Two {@link BooleanFormula}s are {@linkplain BooleanFormula#recordCachingInfo annotated}
     * with {@link BoolTemplateInstance}s that have the same {@link #templCacheId} if grounding out these
     * formulas might yield identical Boolean formulas.
     */
    int getBoolTemplateId() { return templCacheId; }
    
    /**
     * Compute a <code>long</code> value which represents the current values of the arguments
     * of this Boolean template.  The computed value is a compact representation of the binary (boolean)
     * vector obtained by evaluating each bit of {@link #templCacheKey} with the current settings of
     * {@link BoolSwitch} values.  (This method is called while we're traversing a Boolean DAG, and
     * the current settings of the {@link BoolSwitch}es are determined by the {@linkplain SetVarExpr switch setter}
     * nodes we have visited and not yet backtracked from.)  The computed value depends on the current {@linkplain BoolSwitch#getVarValue value}s
     * of the {@linkplain BoolSwitch switches} on which the {@linkplain VarConst switchable constants} referenced
     * by the {@link BooleanFormula}s in {@link #templCacheKey} {@linkplain VarConst#var depend}.
     * The actual value is compressed using the information in {@link #templArgScopes} and {@link #templArgMults},
     * to make it more likely that it will fit inside a <code>long</code>.
     * 
     * Same as BL_CacheExpr::computeCacheKey() in SatLab/src/BL/BL_CachExpr.cc
     */
    long computeTemplKey() {
	Dbg.chk(templArgScopes.length == templArgMults.length);
	long templKey = 0;  // the key we're building
	long argOffset = 0; // the bit offset to which to shift the current arg before it is OR'ed with templKey
	int argStart = 0; // the offset in templCacheKey[] at which the bits of the current argument start
	for (int argNum = 0; argNum < templArgScopes.length; argNum++) {
	    int argMult = templArgMults[argNum];
	    int argScope = templArgScopes[argNum];
	    long argVal = 0;
	    for (int argBitNum = 0; argBitNum < argScope; argBitNum++) {
		// evaluate the current bit of the current argument, using the current settings of Boolean switches.
		// this yields a boolean (binary) value.
		long argBitVal = templCacheKey[argStart + argBitNum].interpret() ? 1 : 0;
		
		if (argMult == BooleanFormula.MULT_SET) {
		    Dbg.chk(((argBitVal << argBitNum) >> argBitNum) == argBitVal);
		    argVal |= (argBitVal << argBitNum);
		} else {
		    if (argBitVal > 0) {
			argVal = (argMult == BooleanFormula.MULT_OPTION) ? argBitNum+1 : argBitNum;
			break;
		    }
		}  // the arg is either an option or a scalar
	    }  // loop over bits of arg
	    
	    Dbg.chk(((argVal << argOffset) >> argOffset) == argVal);
	    templKey |= (argVal << argOffset);
	    argOffset += (argMult==BooleanFormula.MULT_SET ? argScope :
			  Util.binaryLogUp(argScope + (argMult==BooleanFormula.MULT_OPTION ? 1 : 0)));
	    
	    argStart += argScope;
	}  // loop over args
	Dbg.chk(argStart == templCacheKey.length);
	return templKey;
    }  // computeTemplKey()
    
    public String toString() { return "[BoolTemplInst: " + templCacheId + "]"; }
}  // class BoolTemplateInstance

